should{-}forward(${\it es}$; ${\it In}$; ${\it isupdate}$; $f$; $a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$(($\uparrow$($a$ $\in_{b}$ ${\it In}$)) \& ($\uparrow$(${\it isupdate}$(${\it In}$($a$))))) $\vee$ (($\neg$($\uparrow$($a$ $\in_{b}$ ${\it In}$))) \& ($\neg$(loc($f$($a$)) = loc($a$))))